Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    a(lambda(x),y)  → lambda(a(x,p(1,a(y,t))))
2:    a(p(x,y),z)  → p(a(x,z),a(y,z))
3:    a(a(x,y),z)  → a(x,a(y,z))
4:    lambda(x)  → x
5:    a(x,y)  → x
6:    a(x,y)  → y
7:    p(x,y)  → x
8:    p(x,y)  → y
There are 9 dependency pairs:
9:    A(lambda(x),y)  → LAMBDA(a(x,p(1,a(y,t))))
10:    A(lambda(x),y)  → A(x,p(1,a(y,t)))
11:    A(lambda(x),y)  → P(1,a(y,t))
12:    A(lambda(x),y)  → A(y,t)
13:    A(p(x,y),z)  → P(a(x,z),a(y,z))
14:    A(p(x,y),z)  → A(x,z)
15:    A(p(x,y),z)  → A(y,z)
16:    A(a(x,y),z)  → A(x,a(y,z))
17:    A(a(x,y),z)  → A(y,z)
The approximated dependency graph contains one SCC: {10,12,14-17}.
Tyrolean Termination Tool  (0.08 seconds)   ---  May 4, 2006